A:Type, eq:EqDecider(A), x:A, v,z:top. sqequal(fpf-cap(fpf-single(x; v); eq; x; z); v) 

latex

Definitions	x:A. B(x), fpf-cap(f; eq; x; z), fpf-single(x; v), fpf-dom(eq; x; f), deq-member(eq; x; L), t.1, reduce(f; k; as), Y, sq_type(T), P  Q, guard(T), t  T, prop{i:l}, eqof(d), if b then t else f fi , bor(p; q), tt, fpf-ap(f; eq; x), t.2, EqDecider(T), , P  Q, Unit, P  Q, A, False, , ff
Lemmas	bool sq, bool wf, eqof wf, btrue wf, top wf, deq wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot